Lambda the Ultimate

An interesting writeup of the GC techniques used in DrScheme.

3m [the newer "moving memory manager"] definitely works better than [the current] CGC for SirMail, and in principle it should always work at least as well as CGC. Despite having a 3m that works well enough for SirMail for many years, however, we have not yet switched to it as the main build.

Quite interesting for those interested in implementation techniques or using DrScheme. Since GC seems to be a hot topic in the forum these day, I suspect many will want to check this out.

New status report on the R6RS effort (also available as PDF).

Previous LtU discussion (March 2006).

Securing the .NET Programming Model. Andrew J. Kennedy.

The security of the .NET programming model is studied from the standpoint of fully abstract compilation of C#. A number of failures of full abstraction are identified, and fixes described. The most serious problems have recently been fixed for version 2.0 of the .NET Common Language Runtime.

This is highly amusing stuff, of course. Some choice quotes:

if source-language compilation is not fully abstract, then there exist contexts (think ‘attackers’) in the target language that can observably distinguish two program fragments not distinguishable by source contexts. Such abstraction holes can sometimes be turned into security holes: if the author of a library has reasoned about the behaviour of his code by considering only source-level contexts (i.e. other components written in the same source language), then it may be possible to construct a component in the target language which provokes unexpected and damaging behaviour.

One could argue that full abstraction is just a nicety; programmers don’t really reason about observations, program contexts, and all that, do they? Well, actually, I would like to argue that they do. At least, expert programmers...

"A C# programmer can reason about the security properties of component A by considering the behaviour of another component B written in C# that “attacks” A through its public API." -
This can only be achieved if compilation is fully abstract.

To see the six problems identified by thinking about full abstraction you'll have to go read the paper...

In the wake of recent events we decided it is time to hash out a document trying to establish some basic rules of behaviour for LtU discussions.

I've enhanced the FAQ and we have created two new pages. First, there is a new policies page which tries to give some basic ground rules which should help orient new members and be useful in group moderation (i.e., the process in which old timers mentor new members on the appropriate style for LtU discussion by commenting on their posts). The second page, nicknamed the spirit page contains a set of quotes taken from the statements of LtU members over the years which may help explain the way many of us see LtU, and why we care about it both as a discussion venue and a community.

I should emphasize that the goal of these documents is not to change LtU. The goal is to strengthen those traits that made LtU what it is, and try to reduce the friction cause by misunderstandings. Thus the policies document is rather conservative and is mainly a summary of ideas posted previously.

LtU is a community site, and as I am quoted as saying in the spirit page the longer you are a member and contributor the larger the impact you have on the topics under discussion and on the nature of the site in general. Thus, this post is meant to encourage members to raise the voices and tell me what they think of the policies document. It is obviously meant as a draft, for the community to respond to. Let us know if you think something is missing, overstated or simply not to your tastes. I remind you that the goal at this point is not to change the direction of LtU, so if you don't like LtU this is definitely not the opportunity to try and change it. However if you feel you are a member of the community, this is your chance to help.

Finally, let me thank Anton who did most of the hard work putting these pages together. Without his help I wouldn't have managed to get these documents out of the door. While Anton did most of the work, I am of course to blame for anything you might find objectionable.

Microsoft recently announced the Microsoft Robotics Studio, which aims to offer end-to-end robotics development environment customer technical preview for hobbyist, academic, and commercial developers.

This isn't a programming languiage item per se, of course, but I think fun platforms sometimes offer intereseting opportunities (which is why I posted on LEGO Mindstorms before), and I wanted to flush the RSS feed with a new item to test if it's working properly.

We are seeking comments on the final draft of our ICFP 2006 paper: Delimited dynamic binding, by Oleg Kiselyov, Chung-chieh Shan, and Amr Sabry.

Dynamic binding and delimited control are useful together in many settings, including Web applications, database cursors, and mobile code. We examine this pair of language features to show that the semantics of their interaction is ill-defined yet not expressive enough for these uses.

We solve this open and subtle problem. We formalise a typed language DB+DC that combines a calculus DB of dynamic binding and a calculus DC of delimited control. We argue from theoretical and practical points of view that its semantics should be based on delimited dynamic binding: capturing a delimited continuation closes over part of the dynamic environment, rather than all or none of it; reinstating the captured continuation supplements the dynamic environment, rather than replacing or inheriting it. We introduce a type- and reduction-preserving translation from DB+DC to DC, which proves that delimited control macro-expresses dynamic binding. We use this translation to implement DB+DC in Scheme, OCaml, and Haskell.

We extend DB+DC with mutable dynamic variables and a facility to obtain not only the latest binding of a dynamic variable but also older bindings. This facility provides for stack inspection and (more generally) folding over the execution context as an inductive data structure.

The paper comes with a large amount of accompanying code—in Scheme, OCaml, SML, and Haskell. The code (described in the paper's appendix) uses realistic examples to show how the joint behavior of delimited continuations and dynamic binding is ill-defined in various PL systems, and solves the problem by a full-fledged implementation of dynamic binding in all these systems. Any comments or suggestions would be very welcome!

This is, to our knowledge, the first large site to run the PLT Scheme web server continuously for any length of time. Over the next few days we'll provide a few more details about the more intricate parts of our setup so other intrepid pioneers can learn from our work.

It's always good to hear of success stories of non-mainstream languages (well, non-mainstream outside LtU that is), so this project is worth keeping an eye on. Maybe Noel will be able to provide more technical details at some point.

The Charles Babbage Institute is an historical archives and research center of the University of Minnesota. CBI is dedicated to promoting study of the history of information technology and information processing and their impact on society. CBI preserves relevant historical documentation in all media, conducts and fosters research in history and archival methods, offers graduate fellowships, and sponsors symposia, conferences, and publications.

Mission

CBI historians design and administer research projects in the history of information technology and engage in original research that is disseminated through scholarly publications, conference presentations, and the CBI web site. CBI archivists collect, preserve, and make available for research primary source materials relating to the history of information technology. The archival collection consists of corporate records, manuscript materials, records of professional associations, oral history interviews, trade publications, periodicals, obsolete manuals and product literature, photographs, films, videos, and reference materials. CBI also serves as a clearinghouse for resources on the history of information technology.

(Copied from the "about section" of the CBI site, hope that is allowed)

Didn't find any reference to this site on Ltu. Guess it might be of interest to the history department.

A Mobility Calculus with Local and Dependent Types, by Mario Coppo, Federico Cozzi, Mariangiola Dezani-Ciancaglini, Elio Giovannetti and Rosario Pugliese

Abstract:

We introduce an ambient calculus that combines ambient mobility with process mobility, uses group names to group ambients with homologous features, and exploits co-moves and runtime type checking to implement flexible policies for controlling process activities. Types rely on group names and, to support dynamicity, may depend on group variables. Policies can dynamically change also through installation of co-moves. The compliance with ambient policies can be checked locally to the ambients and requires no global assumptions. We prove that the type assignment system and the operational semantics of the calculus are ‘sound’, and we define a sound and complete type inference algorithm which, when applied to terms whose type decorations only express the desired policies, computes the minimal type annotations required for their execution.
As an application of our calculus, we present a couple of examples and linger on the setting up of policies for controlling the activities of the objects involved.

Variance and Generalized Constraints for C# Generics. Burak Emir, Andrew J. Kennedy, Claudio Russo, Dachuan Yu. July 2006

Generic types in C# behave invariantly with respect to sub-typing. We propose a system of type-safe variance for C# that supports the declaration of covariant and contravariant type parameters on generic types. To support more widespread application of variance we also generalize the existing constraint mechanism with arbitrary subtype assertions on classes and methods. This extension is useful even in the absence of variance, and subsumes equational constraints proposed for Generalized Algebraic Data Types (GADTs). We formalize the subtype relation in both declarative and syntax-directed style, and describe and prove the correctness of algorithms for constraint closure and subtyping. Finally, we formalize and prove a type safety theorem for a featherweight language with variant classes and generalized constraints.

Discussion of previous C# GADT paper on LtU.

I am unsure about use-site versus definition-site variance declerations. It would be interesting to hear what others think.

Also check out the LtU discussion on wildcards in Java.